ds:x:Id fp Type, T:Type, x:Id,
f:((State(ds)TDeclaredType(ds;x)) + (State(ds)TDeclaredType(ds;x))).
T  xdom(ds). A=ds(x)   A  (x  dom(ds)) 

latex

Definitions	{T}, SQType(T), State(ds), Top, ff, tt, if b then t else f fi , f(x)?z, x,y. t(x;y), x. t(x), , t  T, P  Q, x:A. B(x), False, A, P  Q, DeclaredType(ds;x), xdom(f). v=f(x)   P(x;v), P & Q, P  Q, Unit, , x(s1,s2), x(s), S  T,
Lemmas	int inc rationals, bool sq, bool cases, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool wf, fpf wf, rationals wf, decl-type wf, decl-state wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, id-deq wf, Id wf, fpf-all wf